T:Type, l1:(T List), v:T, l2:(T List).
fseg(T;l1;l2)  ((||l1|| < ||l2||) c (l2[(||l2|| - (||l1||+1))] = v))  fseg(T;[v / l1];l2) 

latex

ProofTree

Definitions	x:A  B(x), x:A. B(x), x:AB(x), P  Q, x:A. B(x), ||as||, True, Void, False, Type, type List, s = t, a < b, {x:A| B(x)} , , , |g|, S  T, t  T, , [], as @ bs, #$n, n+m, n - m, l[i], x:A.B(x), Top, s ~ t, {T}, SQType(T), [car / cdr], P & Q, P  Q, P  Q, A  B, i  j , A List, A c B, fseg(T;L1;L2), null(as), b, A, last(L), T, -n
Lemmas	select append front, length append, le wf, squash wf, iff wf, rev implies wf, append assoc, last wf, select wf, append wf, not wf, false wf, non neg length, cons one one, guard wf, nat wf, length wf nat, top wf, length wf1, member wf, true wf, last lemma